This article lists model checking tools classified by some interesting properties. Some articles about: history[1] and introduction[2] to Model Checking. There are some books[3] that deal with model checking techniques.
Contents |
Name | Model Checking | Equivalence checking | GUI | Availability | |||||||
---|---|---|---|---|---|---|---|---|---|---|---|
Plain, Probabilistic, Stochastic, ... | Modelling language | Properties language | Supported equivalences | Counter example generation | GUI | Graphical Specification | Counter example visualization | Software license | Programming language used | Platform / OS | |
APMC | Approximate Probabilistic | Reactive modules | PCTL, PLTL | No | Yes | No | No | FUSC | C | Unix & related | |
ARC | Plain | AltaRica | μ-calculus CTL* | Yes | Yes | No | No | FUSC | ANSI C | Unix & related | |
BANDERA | Code analysis | Java | CTL, LTL | Yes | Yes | Yes | Yes | Free | Java | Windows and Unix related | |
BLAST | Code analysis | C | Monitor automata | Yes | No | No | No | Free | OCaml | Windows and Unix related | |
CADENCE SMV | Plain | Cadence SMV, SMV, Verilog | CTL, LTL | Yes | Yes | No | No | FUSC | ? | Windows and Unix related | |
CADP | Probabilistic | LOTOS, FSP, LOTOS NT | AFMC | SB, WB, BB, OE, STE, WTE, SE, tau*E | Yes | Yes | Yes | Yes | FUSC | ? | MacOS, Linux, Solaris, Windows |
CBMC | Code analysis | C, C++ | Assertions | Yes | Yes | No | No | Free | C++ | Windows and Unix related | |
CPAchecker | Code analyses | C | Monitor automata | Yes | Yes | No | ? | Free | Java | Any | |
CWB-NC | Plain and Timed | CCS, CSP, LOTOS, TCCS | AFMC, CTL, GCTL | SB, WB, me, ME | Yes | Yes | No | No | FUSC | SML of New Jersey | Windows and Unix related |
DBRover | Timed | Ada, C, C++, Java, VHDL, Verilog | LTL, MTL | No | Yes | Yes | Yes | Non-freeCommercial use only | ? | Windows and Unix related | |
DiVinE Tool | Plain | DVE input language | LTL | Yes | Yes | No | Yes | Free | C/C++ | Unix, Windows | |
DREAM | Real-time | C++, Timed automata | Monitor automata | Yes | No | No | No | Free | C++ | Windows and Unix related | |
Edinburgh CWB | Plain | CCS, TCCS, SCCS | μ-calculus | SB, WB, BB, me, ME, OE | Yes | No | No | No | FUSC | SML | Windows and Unix related |
EmbeddedValidator | Hybrid | Simulink/Stateflow/TargetLink/C | Monitor automata | Yes | Yes | Yes | Yes | Non-freeCommercial use only | ? | Windows | |
Expander2 | Hybrid | AFMC, CTL | SB, OE | No | Yes | No | No | Free | O'Haskell | Unix related | |
Fc2Tools | Plain | FC2 | ? | SB, WB, BB | Yes | No | Yes | Yes | Free | ? | Unix related |
GEAR | Plain | ? | AFMC, CTL, μ-calculus | Yes | Yes | Yes | Yes | Free | Java | Windows and Unix related | |
ImProve | Plain | Haskell | Assertions | Yes | No | No | No | Free | Haskell | Linux, Windows, Mac-OS | |
LTSA | Plain | FSP | LTL | Yes | Yes | No | Yes | Free | ? | Windows and Unix related | |
LTSmin | Plain | Promela, mCRL2, NIPS-VM, DVE Input Language | μ-calculus, LTL, CTL* | SB, BB | Yes | No | No | No | Free | C | Unix related |
MCMAS | Plain, Epistemic | ISPL | CTL, CTLK | Yes | Yes | No | Yes | Free | C++ | Unix, Windows, Mac-OS | |
mCRL2 | Real-time | mCRL2 | mCRL2 mu-calculus | SB, BB, t*E, STE, WTE | Yes | Yes | No | Yes | Free | C++ | MacOS, Linux, Solaris, Windows |
MRMC | Real-time, Probabilistic | Plain MC | CSL, CSRL, PCTL, PRCTL | SB | No | No | No | No | Free | C | Windows, Linux, MacOS |
NuSMV | Plain | SMV | CTL, LTL, PSL | Yes | No | No | No | Free | C | Unix, Windows, MacOSX | |
ompca, OpenMP C Analysis | software symbolic simulation with API control | C/C++ programs with OpenMP directives | logic predicates or flexible procedures through API | Yes | Yes | No | Yes | Free | C, C++ | Ubuntu Linux, Windows version available soon | |
PAT | Plain,Real-time,Probabilistic | CSP#, Timed CSP, Probablilistic CSP | LTL, Assertions | Yes | Yes | Yes | Yes | Free | C# | Windows, other OS with Mono | |
PRISM | Probabilistic | PEPA, PRISM language, Plain MC | CSL, PLTL, PCTL | No | Yes | No | No | Free | C++, Java | Windows, Linux, MacOS | |
Reactis Tester | Hybrid | Simulink/Stateflow | ? | No | Yes | Yes | No | Non-freeCommercial use only | ? | Windows, Linux | |
RED | dense-time, linear hybrid, fully symbolic | communicating timed automata (CTA), linear-hybrid automata (LHA) | TCTL with fairness assumptions, CTA with fairness assumptions | timed simuilation, fair simulation | Yes | Yes | Yes | Yes | Free | C/C++ | Unbuntu Linux |
SATABS | Code analysis | C, C++ | Assertions | Yes | Yes | No | No | Free | C++ | Windows and Unix related | |
SLMC | Plain | pi-calculus | CCL | Yes | No | No | No | Free | OCAML | Windows and Unix related | |
SPIN | Plain | Promela | LTL | Yes | Yes | No | Yes | FUSC | C, C++ | Windows and Unix related | |
TAPAs | Plain | CCSP | CTL, μ-calculus | SB, WB, BB, STE, WTE, me, ME, OE | Yes | Yes | Yes | Yes | Free | Java | Windows, MacOS and Unix related |
UPPAAL | Real-time | Timed automata, C subset | TCTL subset | No | Yes | Yes | Yes | FUSC | C++, Java | MacOS, Windows, Linux | |
ROMEO | Real-time | Time Petri Nets, stopwatch parametric Petri nets | TCTL subset | Yes | Yes | Yes | No | Free | C++, tcl/tk | MacOS, Windows, Linux | |
TLC | PLAIN | TLA+, PlusCal | TLA | Yes | Yes | Yes | No | Free | Java | Windows, Linux |
Equivalences:
Software license: